\begin{tabbing}
next{-}world{-}state($D$;$i$;$s$;$k$;$v$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\langle$($\lambda$$x$.M($i$).ef($k$,$x$,$s$,$v$)?$s$($x$))\+
\\[0ex]$,\,$doact($k$;$v$)
\\[0ex]$,\,$filter($\lambda$$m$.source(mlnk($m$)) = $i$;M($i$).sends($k$,$s$,$v$))$\rangle$
\-
\end{tabbing}